%% LyX 2.3.6 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[brazil,oldfontcommands]{memoir}
\usepackage{lmodern}
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\usepackage{xcolor}
\definecolor{page_backgroundcolor}{rgb}{1, 1, 1}
\pagecolor{page_backgroundcolor}
\definecolor{document_fontcolor}{rgb}{0, 0, 0}
\color{document_fontcolor}
\usepackage{babel}
\usepackage{prettyref}
\usepackage{calc}
\usepackage{mathrsfs}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\OnehalfSpacing
\usepackage[unicode=true,
 bookmarks=false,
 breaklinks=true,pdfborder={0 0 0},pdfborderstyle={},backref=page,colorlinks=true]
 {hyperref}
\hypersetup{
 hidelinks,pdfcreator={LaTeX via pandoc}}

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
\theoremstyle{plain}
\ifx\thechapter\undefined
	\newtheorem{thm}{\protect\theoremname}
\else
	\newtheorem{thm}{\protect\theoremname}[chapter]
\fi
\theoremstyle{definition}
\newtheorem{defn}[thm]{\protect\definitionname}
\theoremstyle{definition}
\newtheorem{example}[thm]{\protect\examplename}
\theoremstyle{plain}
\newtheorem{prop}[thm]{\protect\propositionname}
\theoremstyle{plain}
\newtheorem{lem}[thm]{\protect\lemmaname}

\@ifundefined{date}{}{\date{}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usepackage{pxfonts}
\usepackage{tikz}
\usepackage[usenames,dvipsnames]{pstricks}
\usepackage{epsfig}
\usepackage{pst-grad} % For gradients
\usepackage{pst-plot} % For axes
\usepackage[space]{grffile} % For spaces in paths
\usepackage{etoolbox} % For spaces in paths
\makeatletter % For spaces in paths
\patchcmd\Gread@eps{\@inputcheck#1 }{\@inputcheck"#1"\relax}{}{}
\makeatother
\newtheorem*{problem*}{\protect\problemname}
\providecommand{\problemname}{Problema}
\usepackage[dvipsnames]{xcolor} 	% para cores
\makeatletter
\hypersetup{
     	%pagebackref=true,
pdftitle={\@title}, 
pdfauthor={\@author},
  %  	pdfsubject={\imprimirpreambulo},
    pdfcreator={LaTeX with abnTeX2},
pdfkeywords={abnt}{latex}{abntex}{abntex2}{livro}, 
colorlinks=true,       		% false: boxed links; true: colored links
    	linkcolor=blue,          	% color of internal links
    	citecolor=blue,        		% color of links to bibliography
    	filecolor=magenta,      		% color of file links
urlcolor=blue,
bookmarksdepth=4
}
\makeatother

\makeatother

\providecommand{\definitionname}{Defini��o}
\providecommand{\examplename}{Exemplo}
\providecommand{\lemmaname}{Lema}
\providecommand{\propositionname}{Proposi��o}
\providecommand{\theoremname}{Teorema}

\begin{document}
\title{Caixas e diamantes: uma introdu��o aberta � l�gica modal}
\author{Remixado por Richard Zach}

\maketitle
\frontmatter

\tableofcontents*

\chapter{Pref�cio}

\chapter{Introdu��o}

L�gicas modais s�o extens�es da l�gica cl�ssica por meio da introdu��o
dos operadores $\square$ (``caixa'') e $\diamondsuit$ (``diamante''),
que se anexam a f�rmulas. Intuitivamente, $\square$ pode ser lido
como ``necessariamente'' e $\diamondsuit,$como ``possivelmente.
Assim $\square p$ � ``$p$ � necessariamente verdadeira'' e $\diamondsuit p$
� ``$p$ � possivelmente verdadeira''. Uma vez que necessidade e
possibilidade s�o no��es metaf�sicas fundamentais, l�gica modal �,
obviamente, de grande interesse filos�fico. Ela permite a formaliza��o
de princ�pios metaf�sicos tais como ``$\square p\rightarrow p$''
(se $p$ � necess�ria, ent�o ela � verdadeira) ou ``$\diamondsuit p\rightarrow\square\diamondsuit p$''
(se $p$ � poss�vel, ela � necessariamente poss�vel).

Os operadores $\square$ e $\diamondsuit$ s�o \emph{intensionais}.
Isto significa que a verdade ou falsidade de $\square A$ ou $\diamondsuit A$
n�o dependem apenas da verdade ou falsidade de $A$. Um operador que
n�o � intensional � extensional. A nega��o � extensional: $\neg A$
� verdadeiro se e somente (sse) $A$ � falso; assim, o valor de verdade
de $\neg A$ depende somente do valor de verdade de $A$. $\square$
e $\diamondsuit$ n�o s�o dessa forma. O valor de verdade de $\square A$
ou de $\diamondsuit A$ depende tamb�m do significado de $A$. Embora
a sem�ntica verofuncional seja suficiente para lidar com operadores
extensionais, operadores intensionais como $\square$ e $\diamondsuit$
requerem um tipo diferente de sem�ntica. Uma tal sem�ntica que toma
um lugar central neste livro � a sem�ntica relacional (tamb�m chamada
sem�ntica de mundos poss�veis ou sem�ntica de Kripke).

A l�gica que corresponde � interpreta��o de $\square$ como ``necessariamente''
tem uma sem�ntica que � � relativamente simples: em vez de atribuir
valores de verdade �s vari�veis proposicionais, uma interpreta��o
$\mathbf{M}$ atribui a um conjunto de ``mundos'' a elas --- intuitivamente,
aqueles mundos em que $p$ � interpretado como verdadeiro. Em base
de uma tal interpreta��o, podemos definir uma rela��o de satisfa��o.
A defini��o desta rela��o de satisfa��o torna $\square A$ satisfeita
em um mundo $w$ sse $A$ � satisfeita em \emph{todos} os mundos:
$\mathbf{M},w\Vdash\square A$ sse $\mathbf{M},v\Vdash A$, para todos
os mundos $v$. Isto corresponde � ideia de Leibniz segundo a qual
o que � necessariamente verdadeiro � o que � verdadeiro em qualquer
mundo poss�vel.

``Necessariamente'' n�o � a �nica maneira de se interpretar o operador
$\square$, mas � a padr�o --- ``necessariamente'' e ``possivelmente''
s�o as ent�o chamadas modalidades \emph{al�ticas}. Em outras interpreta��es,
$\square$ � lido como ``� conhecido (por alguma pessoa \emph{A})
que'', como ``alguma pessoa \emph{A} acredita que'', como ``deveria
ser o caso que'' ou como ``sempre ser� verdadeiro que''. Estas
s�o, respectivamente, modalidades epist�micas, dox�sticas, de�nticas
e temporais. Interpreta��es diferentes de $\square$ far� com que
uma mesma f�rmula seja logicamente verdadeira em uma interpreta��o
e n�o logicamente verdadeira em outra; da mesma forma, uma certa infer�ncia
pode ser v�lida em uma interpreta��o e inv�lida na outra. Por exemplo,
tudo que � necess�rio ou tudo que � conhecido � verdadeiro, assim
$\square A\rightarrow A$ � uma verdade l�gica nas interpreta��es
al�tica e epist�mica. Por outro lado, nem tudo que � acredito ou nem
tudo que deveria ser o caso �, de fato, o caso. Dessa forma, $\square A\rightarrow A$
n�o � uma verdade nas interpreta��es dox�stica ou de�ntica.

A fim de lidar com diferentes interpreta��es dos operadores modais,
a sem�ntica � estendida por meio de uma rela��o entre mundos, a ent�o
chamada rela��o de acessibilidade. Ent�o $\mathbf{M},w\Vdash\square A$
sse $\mathbf{M},v\Vdash A$ para todos os mundos $v$ que s�o acess�veis
a partir de $w$. A sem�ntica resultante � bastante vers�til e poderosa
e a ideia b�sica pode ser usada para fornecer interpreta��es sem�nticas
para l�gicas baseadas em outros operadores intensionais. Uma tal l�gica
� a l�gica intuicionista, uma l�gica construtiva baseada no ramo da
matem�tica construtiva de L. E. J. Brouwer. L�gica intuicionista �
filosoficamente interessante por esta raz�o --- ela desempenha um
papel importante na explica��o construtiva da matem�tica {[}in constructive
accounts of mathematics{]}. Michael Dummett, influente fil�sofo ingl�s
do s�culo 20, prop�s a l�gica intuicionista como uma l�gica superior
� l�gica cl�ssica. Uma outra aplica��o dos modelos relacionais � quando
eles s�o usados como sem�ntica para condicionais subjuntivos ou contrafactuais,
uma abordagem que foi desbravada por Robert Stalnaker e David K. Lewis.

Este livro � uma introdu��o � sintaxe, � sem�ntica e � teoria da prova
de l�gicas intensionais. Ela trata apenas de l�gicas proposicionais,
embora edi��es futuras tamb�m lidar�o com l�gicas de predicados. O
material � dividido em tr�s partes: a primeira parte lida com l�gicas
modais normais. Estas s�o l�gicas com os operadores $\square$ e $\diamondsuit$.
Discutimos a sintaxe delas, modelos relacionais e no��es sem�nticas
baseadas nesses modelos (tais como validade e consequ�ncia) e sistemas
de provas (tanto sistemas axiom�ticos como tabl�s). Estabelecemos
alguns resultados sobre estas l�gicas tais como corre��o e completude
dos sistemas de provas considerados e discutimos algumas constru��es
modelo-te�ricos {[}model-theoretic construction{]} tais como filtra��es.
A segunda parte trada da l�gica intuicionista. Aqui discutimos dedu��o
natural e deriva��es axiom�ticas, sem�nticas relacionais e topol�gica
e corre��o e completude dos sistemas de provas. A terceira parte lida
com a sem�ntica Lewis-Stalnaker dos condicionais contrafactuais. O
ap�ndice discute algumas ideias e resultados da teoria de conjuntos
e da teoria das rela��es que s�o cruciais para a sem�ntica relacional
assim como recapitula a sintaxe, sem�ntica e teoria da prova da l�gica
proposicional cl�ssica.

\mainmatter

\part{L�gicas modais normais}

\chapter{Sintaxe e sem�ntica das l�gicas normais modais}

\section{Introdu��o}

L�gica modal lida com proposi��es modais e com as rela��es de acarretamento
{[}entailment{]} que ocorre entre elas. Exemplos de proposi��es modais
s�o os seguintes:
\begin{enumerate}
\item � necess�rio que $2+2=4$
\item � necessariamente poss�vel que chova amanh�
\item Se � necessariamente poss�vel que $A$, ent�o � poss�vel que $A$
\end{enumerate}
Possibilidade e necessidade n�o s�o as �nicas modalidades: outros
conectivos un�rios s�o tamb�m classificados como modalidades, por
exemplo, ``deveria ser o caso que $A$'', ``Dana sabe que $A$''
ou ``Dana acredita que $A$''.

A primeira apari��o da l�gica modal ocorre no livro \emph{Da Interpreta��o}
de Arist�teles: ele foi o primeiro a perceber que necessidade implica
possibilidade, mas n�o vice-versa; que possibilidade e necessidade
s�o interdefin�veis; que se $A\wedge B$ � possivelmente verdadeira,
ent�o $A$ � possivelmente verdadeira e $B$ � possivelmente verdadeira,
mas n�o inversamente; e que se $A\rightarrow B$ � necess�ria, ent�o
se $A$ � necess�ria, ent�o $B$ � necess�ria.

A primeira abordagem moderna da l�gica modal foi o trabalho de C.
I. Lewis, que culminou no livro \emph{L�gica Simb�lica} (1932) de
Lewis e Langford. Lewis e Langford estavam insatisfeitos com a representa��o
da implica��o por meio do condicional material: $A\rightarrow B$
� um substituto pobre para ``A implica B''. Em vez disso, eles propuseram
caracterizar implica��o como ``Necessariamente, se $A$, ent�o $B$'',
simbolizada como $A\strictif B$. Tentando isolar diferentes propriedades,
Lewis identificou cinco sistema modais diferentes, \textbf{S1}, \textbf{S2},
\textbf{S3}, \textbf{S4}, \textbf{S5}, sendo as duas �ltimas ainda
usadas.

A abordagem de Lewis e Langford foi puramente sint�tica: eles identificaram
axiomas e regras razo�veis e investigaram o que era deriv�vel por
esses meios. Uma abordagem sem�ntica continuou indescrit�vel por muito
tempo {[}A semantic approach remained elusive for a long time{]},
at� que uma primeira tentativa foi feita por Rudolf Carnap em \emph{Significado
e Necessidade} (1947) usando a no��o de \emph{descri��o de estado},
isto �, uma cole��o de senten�as at�micas (aquelas que s�o ``verdadeiras''
neste estado de descri��o). Depois de apresentar a defini��o de verdade
para senten�as arbitr�rias $A$ {[}After lifting the truth definition
to arbitrary sentences A{]}, Carnap define A como sendo \emph{necessariamente
verdadeira}, se ela � verdadeira em todas as descri��es de estado.
A abordagem de Carnap n�o poderia lidar com modalidades \emph{iteradas},
j� que senten�as da forma ``Possivelmente � necess�rio que $A$ �
poss�vel'' sempre se reduzem � modalidade mais interna {[}innermost{]}.

O maior avan�o {[}breakthrough{]} na sem�ntica modal veio com artigo
``Um teorema da completude na l�gica modal'' (JSL 1959) de Saul
Kripke. Kripke baseou o seu trabalho na ideia de Leibniz segundo a
qual um enunciado � necessariamente verdadeiro se ele � verdadeiro
``em todos os mundos poss�veis''. Esta ideia , entretanto, sofre
das mesmas desvantagens {[}drawbacks{]} que a de Carnap, j� que a
verdade do enunciado em um mundo $w$ (ou em uma descri��o de estado
$s$) n�o depende de $w$ absolutamente. Assim Kripke assumiu que
os mundos est�o relacionados por meio de uma \emph{rela��o de acessibilidade}
$R$ e que um enunciado da forma ``Necessariamente $A$'' � verdadeira
em um mundo $w$ se e somente se $A$ � verdadeiro em todos os mundos
$w'$ acess�veis a partir de $w$. Sem�nticas que ofereceram alguma
vers�o desta abordagem s�o chamadas sem�nticas de Kripke e possibilitaram
o desenvolvimento turbulento {[}tumultuous development{]} das l�gicas
modais (no plural).

Quando interpretada pelas sem�nticas de Kripke, l�gica modal mostra-nos
como s�o as estruturas relacionais ``de dentro''. Uma estrutura
relacional � exatamente um conjunto abastecido com uma rela��o bin�ria
(por exemplo, o conjunto de estudantes na sala de aula ordenados pelo
numera��o da carteira de identidade (ou cpf) � uma estrutura relacional).
Mas, de fato, estruturas relacionais est�o dispon�veis {[}come in{]}
em todos os tipos de dom�nios: al�m da possibilidade relativa dos
estados do mundo, podemos ter estados epist�micos de algum agente
relacionado por possibilidade epist�mica ou ter estados de um sistema
din�mico com as transi��es de estado deles, etc. L�gica modal pode
ser usada para modelar todos estes: a primeira estrutura nos d� l�gica
modal ordin�ria, al�tica; as outras nos s�o l�gica epist�mica, l�gica
din�mica, etc.

Focamos em um �ngulo particular, conhecido pelos l�gicos modais como
``teoria da correspond�ncia''. Uma das mais significantes descobertas
iniciais de Kripke � que muitas propriedades da rela��o de acessibilidade
$R$ (se ela � transitiva, sim�trica, etc) podem ser caracterizadas
\emph{na pr�pria linguagem modal} por meio de ``esquemas modais''
apropriados. L�gicos modais dizem, por exemplo, que a reflexividade
de $R$ ``corresponde'' ao esquema ``Se necessariamente $A$, ent�o
$A$''. Exploramos principalmente a teoria da correspond�ncia de
alguns sistemas cl�ssicos de l�gica modal (por exemplo, \textbf{S4}
e \textbf{S5}) obtidos por meio da combina��o dos esquemas D, T, B,
4 e 5.

\section{A linguagem da l�gica modal b�sica\vspace{8pt}
}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
A linguagem b�sica da l�gica modal cont�m
\end{defn}

\begin{enumerate}
\item A constante proposicional para falsidade $\bot$
\item Um conjunto infinito e enumer�vel de vari�veis proposicionais: $p_{0},p_{1},p_{2},\ldots$
\item Os conectivos proposicionais: $\neg$ (nega��o), $\wedge$ (conjun��o),
$\vee$ (disjun��o), $\rightarrow$ (condicional)
\item O operador modal $\square$
\item O operador modal $\diamondsuit$
\end{enumerate}
%
\end{minipage}}}

\vspace{8pt}
\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
\emph{F�rmulas} da linguagem modal b�sica s�o indutivamente definidas
como se segue
\end{defn}

\begin{enumerate}
\item $\bot$ � uma f�rmula at�mica
\item Qualquer vari�vel proposicional $p_{i}$ � uma f�rmula (at�mica)
\item Se $A$ e $B$ s�o f�rmulas, ent�o $(A\wedge B)$ � uma f�rmula.
\item Se $A$ e $B$ s�o f�rmulas, ent�o $(A\vee B)$ � uma f�rmula.
\item Se $A$ e $B$ s�o f�rmulas, ent�o $(A\rightarrow B)$ � uma f�rmula.
\item Se $A$ � uma f�rmula, ent�o $\square A$ � uma f�rmula
\item Se $A$ � uma f�rmula, ent�o $\diamondsuit A$ � uma f�rmula
\item Nenhuma outra express�o � uma f�rmula
\end{enumerate}
Se a f�rmula $A$ n�o cont�m $\square$ ou $\diamondsuit$, dizemos
que ela � modalmente livre {[}modal-free{]}%
\end{minipage}}}\vspace{8pt}


\section{Substitui��o simult�nea}

Uma inst�ncia de uma f�rmula $A$ � o resultado da substitui��o de
todas as ocorr�ncias de uma vari�vel proposicional em $A$ por alguma
outra f�rmula. Referir-nos-emos frequentemente �s inst�ncias das f�rmulas
tanto ao discutir validade com ao discutir derivabilidade. Portanto
� �til definir a no��o precisamente.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Sejam $A$ uma f�rmula modal em que todas as vari�veis proposicionais
est�o entre $p_{1},\ldots,p_{n}$ e $D_{1},\ldots,D_{n}$ f�rmulas
tamb�m modais, definimos $A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ como
o resultado de substituir simultaneamente cada um dos $p_{i}$ por
$D_{i}$ em $A$. Formalmente, isto � uma defini��o por indu��o sobre
{[}a complexidade de{]} $A$:
\end{defn}

\begin{enumerate}
\item $A\equiv\bot$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $\bot$
\item $A\equiv q$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $q$, dado que
$q\not\equiv p_{i}$ (para $i=1,\ldots,n$).
\item $A\equiv p_{i}$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $D_{i}$
\item $A\equiv\neg B$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $\neg B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
\item $A\equiv(B\wedge C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\wedge C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv(B\vee C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\vee C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv(B\rightarrow C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ �
$(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\rightarrow C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv(B\leftrightarrow C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
� $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\leftrightarrow C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv\square B$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $\square B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
\item $A\equiv\diamondsuit B$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � $\diamondsuit B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
\end{enumerate}
A f�rmula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ � chamada uma inst�ncia
de substitui��o de $A$.%
\end{minipage}}}\vspace{8pt}

\begin{example}
Suponha que $A$ seja $p_{1}\rightarrow\square(p_{1}\wedge p_{2})$,
$D_{1}$, $\diamondsuit(p_{2}\rightarrow p_{3})$ e $D_{2}$, $\neg\square p_{1}$.
Ent�o $A[D_{1}/p_{1},D_{2}/p_{2}]$ � $\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge\neg\square p_{1})$.
Por outro lado, $A[D_{2}/p_{1},D_{1}/p_{2}]$ � $\neg\square p_{1}\rightarrow\square(\neg\square p_{1}\wedge\diamondsuit(p_{2}\rightarrow p_{3}))$.
\end{example}

Note que substitui��o simult�nea n�o �, em geral, o mesmo que substitui��o
iterada, por exemplo, compare $A[D_{1}/p_{1},D_{2}/p_{2}]$ acima
com $(A[D_{1}/p_{1}])[D_{2}/p_{2}]$ que �:
\begin{center}
$\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge p_{2})[\neg\square p_{1}/p_{2}]$,
ou seja,
\par\end{center}

\begin{center}
$\diamondsuit(\neg\square p_{1}\rightarrow p_{3})\rightarrow\square(\diamondsuit(\neg\square p_{1}\rightarrow p_{3})\wedge\neg\square p_{1})$.
\par\end{center}

\noindent E tamb�m compare com $(A[D_{2}/p_{2}])[D_{1}/p_{1}]$
\begin{center}
$p_{1}\rightarrow\square(p_{1}\wedge\neg\square p_{1})[\diamondsuit(p_{2}\rightarrow p_{3})/p_{1}]$,
ou seja,
\par\end{center}

\begin{center}
$\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge\neg\square\diamondsuit(p_{2}\rightarrow p_{3}))$.
\par\end{center}

\section{Modelos relacionais}

O conceito b�sico de sem�ntica para l�gicas modais normais � o de
\emph{modelo relacional}. O modelo consiste em um conjunto de mundos,
que est�o relacionados por meio de uma ``\emph{rela��o de acessibilidade}''
bin�ria, junto com uma atribui��o que determina quais vari�veis proposicionais
contam como ``verdadeiras'' nestes mundos.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Um \emph{modelo} para linguagem modal b�sica � uma tripla ordenada
$\mathbf{M}=<W,R,V>$, em que
\end{defn}

\begin{enumerate}
\item $W$ � um conjunto n�o-vazio de ``mundos'';
\item $R$ � uma rela��o de acessibilidade bin�ria sobre $W$ e;
\item $V$ � uma fun��o que atribui a cada vari�vel proposicional $p$ um
conjunto $V(p)$ de mundos poss�veis.
\end{enumerate}
%
\end{minipage}}}

\vspace{8pt}
Quando $Rww'$ vale, dizemos que $w'$ \emph{� acess�vel a partir
de} $w$. Quando $w\in V(p)$, dizemos que $p$ \emph{� verdadeira
em }$w$.

A grande vantagem da sem�ntica relacional � que modelos podem ser
representados por meio de diagramas simples, tais como o da Figura
\ref{fig:simples}. Mundos s�o representados por n�dulos e o mundo
$w'$ � acess�vel a partir de $w$ exatamente quando h� uma seta de
$w$ em dire��o a $w'$. Al�m disso, rotulamos um n�dulo (mundo) por
$p$ quando $w\in V(p)$. Caso contr�rio, rotulamos o n�dulo por $\neg p$.
A Figura \ref{fig:simples} representa o modelo com $W=\{w_{1},w_{2},w_{3}\},R=\{<w_{1},w_{2}>,<w_{1},w_{3}>\},V(p)=\{w_{1},w_{2}\}$
e $v(q)=\{w_{2}\}$.

\begin{figure}
\begin{centering}
\psscalebox{.7 .7} % Change this value to rescale the drawing. 
{ 
\begin{pspicture}(0,-3.9)(6.14,3.9) 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](0.88,-0.22){0.88} 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.64,3.02){0.88}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.62,-3.02){0.88}
\rput[bl](0.64,-0.32){$w_1$} \rput[bl](4.54,2.9){$w_2$} \rput[bl](4.38,-3.2){$w_3$} \rput[bl](2.04,-0.02){$p$} \rput[bl](1.94,-0.52){$\neg q$} \rput[bl](5.94,3.18){$p$}
\rput[bl](5.9,2.56){$q$} 
\rput[bl](5.74,-2.88){$\neg p$} 
\rput[bl](5.74,-3.42){$\neg q$}
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(1.64,-0.84)(3.6,-2.5) 
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(1.52,0.68)(3.66,2.44)
\end{pspicture} 
}
\par\end{centering}
\caption{Um modelo simples.}

\label{fig:simples}
\end{figure}


\section{Verdade em um mundo}

Qualquer modelo modal determina quais f�rmulas modais contam como
verdadeiras nos mundos dentro do modelo. A rela��o ``modelo $\mathbf{M}$
faz a f�rmula $A$ verdadeira no mundo $w$'' � uma no��o b�sica
de sem�ntica relacional. A rela��o � definida indutivamente e coincide
com a caracteriza��o habitual que usa tabelas de verdade para operadores
n�o-modais.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
\emph{Verdade de uma f�rmula A em} $w$ em um {[}modelo{]} $\mathbf{M}$,
em s�mbolos:
\end{defn}

\begin{enumerate}
\item $A\equiv\bot$: Nunca $\mathbf{M},w\Vdash\bot$;
\item $\mathbf{M},w\Vdash p$ sse $w\in V(p)$;
\item $A\equiv\neg B$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\nVdash B$;
\item $A\equiv(B\wedge C)$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\Vdash B$
e $\mathbf{M},w\Vdash C$;
\item $A\equiv(B\vee C)$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\Vdash B$
ou $\mathbf{M},w\Vdash C$;
\item $A\equiv(B\rightarrow C)$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\nVdash B$
ou $\mathbf{M},w\Vdash C$;
\item $A\equiv\square B$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w'\Vdash B$
para todo $w'\in W$ com $Rww'$;
\item $A\equiv\diamondsuit B$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w'\Vdash B$
para pelo menos um $w'\in W$ com $Rww'$;
\end{enumerate}
%
\end{minipage}}}\vspace{8pt}

Note que, de acordo com a cl�usula 7, uma f�rmula $\square B$ � verdadeira
em $w$, sempre que n�o h� qualquer $w'$ tal que $Rww'$. Em um tal
caso, $\square B$ � vacuamente verdadeiro em $w$. $\square B$tamb�m
pode ser satisfeito em $w$, mesmo se $B$ n�o �. A verdade de $B$
em $w$ n�o garante a verdade de $\diamondsuit B$ em $w$. Isto vale,
entretanto, se $Rww$, ou seja, se $R$� reflexiva. Se n�o h� $w'$
tal que $Rww'$, ent�o $\mathbf{M},w\nVdash\diamondsuit A$, para
qualquer A.
\begin{prop}
1.$\mathbf{M},w\Vdash\square A$ sse $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$

2. $\mathbf{M},w\Vdash\diamondsuit A$ sse $\mathbf{M},w\Vdash\neg\square\neg A$\label{proposicao1.7}
\end{prop}

\begin{proof}
1. $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$ sse $\mathbf{M},w\nVdash\diamondsuit\neg A$por
meio da defini��o de $\mathbf{M},w\Vdash$. $\mathbf{M},w\Vdash\diamondsuit\neg A$
sse para algum $w'$ com $Rww'$, $\mathbf{M},w'\Vdash\neg A$. Logo,
$\mathbf{M},w\nVdash\diamondsuit\neg A$ sse para todo $w'$ com $Rww'$,
$\mathbf{M},w'\nVdash\neg A$. Tamb�m temos que $\mathbf{M},w'\nVdash\neg A$
sse $\mathbf{M},w'\Vdash A$. Juntando, temos que $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$
sse para todo $w'$ com $Rww'$, $\mathbf{M},w'\Vdash A$. Novamente,
pela defini��o de $\mathbf{M},w\Vdash$, isso � o casso sse $\mathbf{M},w\Vdash\square A$.

2. Exerc�cio
\end{proof}
%

\section{Verdade em um modelo}

�s vezes � de interesse investigar quais f�rmulas s�o verdadeiras
em qualquer mundo em uma dado modelo. Introduziremos uma nota��o para
isto.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Uma f�rmula $A$ � verdadeira em um modelo $\mathbf{M}=<W,R,V>$,
escrita $\mathbf{M}\Vdash A$, se e somente se $\mathbf{M},w\Vdash A$
para qualquer $w\in W$.
\end{defn}

%
\end{minipage}}}\vspace{8pt}

\begin{prop}
1. Se $\mathbf{M}\Vdash A$, ent�o $\mathbf{M}\nVdash\neg A$, mas
n�o vice-versa

2. Se $\mathbf{M}\Vdash A\rightarrow B$, ent�o $\mathbf{M}\Vdash A$
somente se $\mathbf{M}\Vdash B$, mas n�o vice-versa
\end{prop}

\begin{proof}
1. Se $\mathbf{M}\Vdash A$, ent�o $A$ � verdadeiro em todos os mundos
poss�veis em $W$ e, uma vez que $W\neq\emptyset$, n�o ser {[}o caso{]}
que $\mathbf{M}\Vdash A$, pois, caso contr�rio, $A$ teria de ser
verdadeiro e falso em algum mundo.

Por outro lado, se $\mathbf{M}\nVdash\neg A$, ent�o $A$ � verdadeiro
em algum mundo $w\in W$. N�o se segue que $\mathbf{M},w\Vdash A$,
\emph{para qualquer} $w\in W$. Por exemplo, no modelo da Figura \ref{fig:simples},
$\mathbf{M}\nVdash\neg p$ e tamb�m $\mathbf{M}\nVdash p$.

2. Assuma que $\mathbf{M}\Vdash A\rightarrow B$ e $\mathbf{M}\Vdash A$;
mostre que $\mathbf{M}\Vdash B$. Seja $w$ um mundo arbitr�rio. Ent�o
$\mathbf{M},w\Vdash A\rightarrow B$ e $\mathbf{M},w\Vdash A$, assim
$\mathbf{M},w\Vdash B$. Uma vez que $w$ era arbitr�rio, $\mathbf{M}\Vdash B$.

Para mostrar que a inversa falha, precisamos encontrar um modelo $M$
tal que $\mathbf{M}\Vdash A$ somente se $\mathbf{M}\Vdash B$, mas
$\mathbf{M}\nVdash A\rightarrow B$. Considere novamente o modelo
da Figura \ref{fig:simples}: $\mathbf{M}\nVdash p$ e, portanto,
(vacuamente) $\mathbf{M}\Vdash p$ somente se $\mathbf{M}\Vdash q$.
Entretanto, $\mathbf{M}\nVdash p\rightarrow q$, pois $p$ � verdadeiro,
mas $q$ � falso em $w_{1}$.
\end{proof}
%

\section{Validade}

F�rmulas que s�o verdadeiras em todos os modelos, isto �, verdadeiras
em qualquer mundo em qualquer modelo, s�o particularmente interessantes.
Elas representam aquelas proposi��es modais que s�o verdadeiras independentemente
de como $\square$ e $\diamondsuit$ s�o interpretados, contanto que
a interpreta��o seja ``normal'' no sentido em que ela � gerada por
alguma rela��o de acessibilidade sobre mundos poss�veis. Chamamos
tais f�rmulas \emph{v�lidas}. Por exemplo, $\square(p\wedge q)\rightarrow\square p$
� v�lida. Algumas f�rmulas que esperar�amos como sendo v�lida em base
da interpreta��o al�tica de $\square$ n�o s�o, entretanto, v�lidas.
Parte do interesse de modelos relacionais � que interpreta��es diferentes
de $\square$ e $\diamondsuit$ podem ser capturadas por diferentes
tipos de rela��es de acessibilidade. Isto sugere que dever�amos definir
validade n�o apenas relativa a todos \emph{os modelos}, mas tamb�m
relativa a todos os modelos \emph{de um certo tipo}. Ser� visto, por
exemplo, que {[}It will turn out, e. g., that{]} $\square p\rightarrow p$
� verdadeira em todos os modelos em que qualquer mundo � acess�vel
a partir de si mesmo, ou seja, quando $R$ � reflexiva. Definir validade
relativa a classes de modelos capacita-nos a formular isto de forma
sucinta: $\square p\rightarrow p$ � v�lida na classe de modelos reflexivos.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Uma f�rmula $A$ \emph{� v�lida} em uma classe $\mathscr{C}$ de modelos,
se ela � verdadeira em qualquer modelo em $\mathscr{C}$ (ou seja,
verdadeira em qualquer mundo em qualquer modelo em $\mathscr{C}$).
Se $A$ � v�lida em $\mathscr{C}$, escrevemos $\mathscr{C}\models A$
e escrevemos $\models A$, se $A$ � v�lido na classe de \emph{todos}
os modelos.
\end{defn}

%
\end{minipage}}}\vspace{8pt}

\begin{prop}
Se $A$ � v�lida em $\mathscr{C}$, ent�o ela � tamb�m v�lida em cada
classe $\mathscr{C}'\subseteq\mathscr{C}$.
\end{prop}

\begin{prop}
Se $A$ � v�lida, ent�o $\square A$ � v�lida
\end{prop}

\begin{proof}
Assuma que $\models A$. Mostre que $\models\square A$. Seja $\mathbf{M}=<W,R,V>$
um modelo e $w\in W$. Se $Rww'$, ent�o $\mathbf{M},w'\Vdash A$,
uma vez que $A$ � v�lida e, assim, $\mathbf{M},w'\Vdash\square A$.
Uma vez que $\mathbf{M}$ e $w$ s�o arbitr�rios, ent�o $\models\square A$.
\end{proof}
%

\section{Inst�ncias tautol�gicas}

Uma f�rmula modalmente livre {[}modal-free formula{]} se ela � verdadeira
sob qualquer atribui��o de valor de verdade. Claramente qualquer tautologia
� verdadeira em qualquer mundo em qualquer modelo. Mas, para as f�rmulas
que envolvem $\square$ e $\diamondsuit$, a no��o de tautologia n�o
� definida. Por exemplo, $\square p\vee\neg\square p$ --- uma inst�ncia
do princ�pio do terceiro exclu�do --- � v�lido? A no��o de \emph{inst�ncia
tautol�gica} ajuda: uma f�rmula que � uma inst�ncia de substitui��o
de uma tautologia (n�o modal). N�o � surpreendente, mas ainda requer
prova, o fato de que qualquer inst�ncia tautologia seja v�lida.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Uma f�rmula $B$ � uma inst�ncia tautol�gica se e somente se h� uma
tautologia modalmente livre {[}modal-free tautology{]} $A$ com vari�veis
proposicionais $p_{1},\ldots,p_{n}$ e f�rmulas $D_{1},\ldots D_{n}$
tal que $B\equiv A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

\begin{lem}
\label{lema14}Suponha que $A$ seja uma f�rmula modalmente livre
cujas vari�veis proposicionais s�o $p_{1},\ldots,p_{n}$ e sejam $D_{1},\ldots,D_{n}$
f�rmulas modais. Ent�o para qualquer atribui��o $\mathcal{V}$, qualquer
modelo $\mathbf{M}=<W,R,V>$ e qualquer $w\in W$ tal que $\mathcal{V}(p_{i})=\mathrm{T}$
se e somente se $\mathbf{M},w\Vdash D_{i}$, temos que $v\models A$
se e somente se $\mathbf{M},w\Vdash A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$.
\end{lem}

\begin{proof}
Por indu��o sobre $A$. 1. $A\equiv\bot$: Tanto $\mathcal{V}\nvDash\bot$
como $\mathbf{M},w\models\bot$ \\2. $A\equiv p_{i}$:\\%
\begin{tabular}{ccll}
$\mathcal{V}\models p_{i}$ & $\Longleftrightarrow$ & $\mathcal{V}(p_{i})=\mathrm{T}$ & pela defini��o de $\mathcal{V}\models p_{i}$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash D_{i}$ & pela hip�tese;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash p_{i}[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pois $p_{i}[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$.\tabularnewline
\end{tabular}\\3. $A\equiv\neg B$:\\%
\begin{tabular}{ccll}
$\mathcal{V}\models\neg B$ & $\Longleftrightarrow$ & $\mathcal{V}\nvDash\mathrm{B}$ & pela defini��o de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\nVdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hip�tese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash\neg B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela def. de $\mathcal{V}\models$.\tabularnewline
\end{tabular}\\4. $A\equiv(B\wedge C)$:\\%
\begin{tabular}{ccll}
$\mathcal{V}\models B\wedge C$ & $\Longleftrightarrow$ & $\mathcal{V}\models B$ e $\mathcal{V}\models C$ & pela defini��o de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ e  & \tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hip�tese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash(B\wedge C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela defini��o de $\mathbf{M},w\Vdash$\tabularnewline
\end{tabular}\\5. $A\equiv(B\vee C)$: \\%
\begin{tabular}{ccll}
$\mathcal{V}\models B\vee C$ & $\Longleftrightarrow$ & $\mathcal{V}\models B$ ou $\mathcal{V}\models C$ & pela defini��o de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ ou & \tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hip�tese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash(B\vee C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela defini��o de $\mathbf{M},w\Vdash$\tabularnewline
\end{tabular}\\6. $A\equiv(B\rightarrow C)$: \\%
\begin{tabular}{ccll}
$\mathcal{V}\models B\rightarrow C$ & $\Longleftrightarrow$ & $\mathcal{V}\nvDash B$ ou $\mathcal{V}\models C$ & pela defini��o de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\nVdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ ou & \tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hip�tese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash(B\rightarrow C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela defini��o de $\mathbf{M},w\Vdash$\tabularnewline
\end{tabular}
\end{proof}
%
\begin{prop}
Todas as inst�ncias tautol�gicas s�o v�lidas
\end{prop}

\begin{proof}
Vamos prova a contrapositiva. Suponha que $A$ � tal que $\mathbf{M},w\nVdash A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
para algum modelo $\mathbf{M}$ e algum mundo $w$. Defina uma atribui��o
$\mathcal{V}$ tal que $\mathcal{V}(p_{i})=\mathrm{T}$ se e somente
se $\mathbf{M},w\Vdash D_{i}$(e $\mathcal{V}$ atribui valores arbitr�rios
a $q\notin\{p_{1},\ldots,p_{n}\}$). Ent�o pelo Lema \ref{lema14},
$\mathcal{V}\nvDash A$ e, assim, $A$ n�o � tautologia.
\end{proof}
%

\section{Esquemas e validade}

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Um esquema � um conjunto de f�rmulas que inclui todas e somente {[}\emph{all
and only}{]} as inst�ncias de substitui��o de alguma f�rmula modal
$C$, ou seja, $\{B:\exists D_{1},\ldots,\exists D_{n}(B=C[D_{1}/p_{1},\ldots,D_{n}/p_{n}])\}$
.

A f�rmula $C$ � chamada a f�rmula caracter�stica {[}\emph{characteristic
formula}{]} do esquema e ela � �nica at� {[}up to{]} a renomea��o
das vari�veis proposicionais. Uma f�rmula $A$ � uma inst�ncia de
um esquema, se ela � um membro do conjunto.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

� conveniente denotar um esquema por meio de express�o metalingu�stica
obtida por de meio da substitui��o dos componentes at�micos de $C$
por `$A$', `$B$',$\ldots$.Assim, por exemplo, os seguintes denotam
esquemas: `$A$', `$A\rightarrow\square A$', `$A\rightarrow(B\rightarrow A)$'.
Eles correspondem �s f�rmulas caracter�sticas $p$, $p\rightarrow\square p$,
$p\rightarrow(q\rightarrow p)$. O esquema `$A$' denota o conjunto
de \emph{todas} as f�rmulas.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Um esquema ser� \emph{verdadeiro }em um modelo se e somente se todas
as suas inst�ncias forem verdadeiras no modelo; e um esquema ser�
v�lido se e somente se ele for verdadeiro em qualquer modelo.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

\begin{prop}
O seguinte esquema K � v�lido:

\begin{equation}
\square(A\rightarrow B)\rightarrow(\square A\rightarrow\square B)\tag{K}
\end{equation}
\end{prop}

\begin{proof}
Precisamos mostrar que todas as inst�ncias do esquema s�o verdadeiras
em qualquer mundo em qualquer modelo. Assim, sejam $\mathbf{M}=<W,R,V>$
e $w\in W$ arbitr�rios. Para mostrar que um condicional � verdadeiro
em um mundo, assumimos que o antecedente � verdadeiro para mostrar
que o consequente � verdadeiro tamb�m, Neste caso, assuma que $\mathbf{M},w\Vdash\square(A\rightarrow B)$
e $\mathbf{M},w\Vdash\square A$. Precisamos mostrar que $\mathbf{M},w\Vdash\square B$.
Assim, seja $w'$ arbitr�rio tal que $Rww'$. Ent�o, pela primeira
suposi��o, temos que $\mathbf{M},w'\Vdash A\rightarrow B$ e, pela
segunda suposi��o, temos que $\mathbf{M},w'\Vdash A$. Logo, segue-se
que $\mathbf{M},w'\Vdash B$. Uma vez que $w'$ era arbitr�rio, temos
que $\mathbf{M},w\Vdash\square B$.
\end{proof}
%
\begin{prop}
O seguinte esquema DUAL \emph{� v�lido\label{proposicao1.19}}

\begin{equation}
\diamondsuit A\leftrightarrow\neg\square\neg A\tag{DUAL}
\end{equation}
\end{prop}

\begin{proof}
Exerc�cio
\end{proof}
%
\begin{prop}
Se $A$ e $A\rightarrow B$ s�o verdadeiras em um mundo, em um modelo,
ent�o $B$ tamb�m �. Assim, as f�rmulas v�lidas s�o fechadas sob modus
ponens.
\end{prop}

\begin{prop}
Uma f�rmula $A$ser� v�lida sse todas as suas inst�ncias de substitui��o
forem tamb�m. Em outras palavras, um esquema � v�lido sse sua f�rmula
caracter�stica tamb�m for. \label{proposicao1.21}
\end{prop}

\begin{proof}
A dire��o ``se'' � �bvia, uma vez que $A$� uma inst�ncia de substitui��o
de si mesma.

Para provar a dire��o ``somente se'', mostramos o seguinte: suponha
que $\mathbf{M}=<W,R,V>$ � um modelo modal e que $B\equiv A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
� uma inst�ncia de substitui��o de $A$. Defina $\mathbf{M'}=<W,R,V'>$
por meio de $V(p_{i})=\{w:\mathbf{M}\Vdash D_{i}w\}$. Ent�o $\mathbf{M}\Vdash Bw$
sse $\mathbf{M'}\Vdash Aw$, para qualquer $w\in W$ (a prova ser�
deixada como exerc�cio). Suponha agora que $A$ era v�lida, mas alguma
inst�ncia de substitui��o $B$ de A n�o era v�lida. Ent�o, para algum
$\mathbf{M}=<W,R,V>$ e algum $w\in W$, $\mathbf{M}\nVdash Bw$.
Mas, ent�o, $\mathbf{M'}\nVdash Aw$ pela reivindica��o e $A$ n�o
� v�lida, uma contradi��o.
\end{proof}
%
Note, entretanto, que n�o � verdadeiro que um esquema seja verdadeiro
em um modelo sse sua f�rmula caracter�stica tamb�m �. Obviamente,
a dire��o ``somente se'' vale: se qualquer inst�ncia de $A$� verdadeira
em $\mathbf{M}$, ent�o a pr�pria $A$ � verdadeira em $\mathbf{M}$.
Contudo, pode acontecer que $A$ seja verdadeira em $\mathbf{M}$,
mas alguma inst�ncia de $A$ seja falsa em algum mundo em $\mathbf{M}$.
Para um contraexemplo muito simples, considere $p$ em um modelo com
apenas um mundo $w$ e $V(p)=\{w\}$, de forma que $p$ � verdadeiro
em $w$. Mas $\bot$ � uma inst�ncia de $p$ e n�o � verdadeiro em
$w$.
\begin{center}
\begin{table}
\centering{}%
\begin{tabular}{|l|l|}
\hline 
Esquemas v�lidos & Esquemas inv�lidos\tabularnewline
\hline 
\hline 
$\square(A\rightarrow B)\rightarrow(\diamondsuit A\rightarrow\diamondsuit B)$ & $\square(A\vee B)\rightarrow(\square A\vee\square B)$\tabularnewline
$\diamondsuit(A\rightarrow B)\rightarrow(\square A\rightarrow\diamondsuit B)$ & $(\diamondsuit A\vee\diamondsuit B)\rightarrow\diamondsuit(A\wedge B)$\tabularnewline
$\square(A\wedge B)\leftrightarrow(\square A\wedge\square B)$ & $A\rightarrow\square A$\tabularnewline
$\square A\rightarrow\square(B\rightarrow A)$ & $\square\diamondsuit A\rightarrow B$\tabularnewline
$\neg\diamondsuit A\rightarrow\square(A\rightarrow B)$ & $\square\square A\rightarrow\square A$\tabularnewline
$\diamondsuit(A\vee B)\leftrightarrow(\diamondsuit A\vee\diamondsuit B)$ & $\square\diamondsuit A\rightarrow\diamondsuit\square A$\tabularnewline
\hline 
\end{tabular}\caption{Esquemas v�lidos e (ou?) inv�lidos\label{tabela1.1}}
\end{table}
\par\end{center}

\section{Acarretamento {[}\emph{entailment}{]}}

Com a defini��o de verdade em um mundo, podemos definir a rela��o
de acarretamento entre f�rmulas. Uma f�rmula $B$ acarreta $A$ sse
sempre que $B$ � verdadeira, $A$ � verdadeira tamb�m. Aqui, ``sempre
que'' significa ``qualquer que seja o modelo que consideramos''
assim como ``qualquer que seja o mundo neste modelo que consideramos''.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Se $\varGamma$ � um conjunto de f�rmulas e $A$ � uma f�rmula, ent�o
$\varGamma$ acareta $A$ --- em s�mbolos: $\varGamma\models A$---
se e somente se para qualquer modelo $\mathbf{M}=<W,R,V>$ e qualquer
mundo $w\in W$, se $\mathbf{M},w\Vdash B$ para qualquer $B\in\varGamma$,
ent�o $\mathbf{M},w\Vdash A$. Se $\varGamma$ cont�m uma �nica f�rmula
$B$, escrevemos $B\models A$.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

\begin{example}
Para mostrar que uma f�rmula acarreta uma outra, temos de raciocionar
sobre todos os modelos, usando a defini��o de $\mathbf{M},w\Vdash$.
Por exemplo, para mostrar que $p\rightarrow\diamondsuit p\models\square\neg p\rightarrow\neg p$,
poder�amos argumentae como se segue: considere um modelo $\mathbf{M}=<W,R,V>$
e $w\in W$ e suponha que $\mathbf{M},w\Vdash p\rightarrow\diamondsuit p$.
Temos de mostrar que $\mathbf{M},w\Vdash\square\neg p\rightarrow\neg p$.
Suponha que isso n�o � o caso. Ent�o $\mathbf{M},w\Vdash\square\neg p$
e $\mathbf{M},w\nVdash\neg p$. Uma vez que $\mathbf{M},w\nVdash\neg p$,
ent�o $\mathbf{M},w\Vdash p$. Pela suposi��o, $\mathbf{M},w\Vdash p\rightarrow\diamondsuit p$,
assim $\mathbf{M},w\Vdash\diamondsuit p$. Pela defini��o de $\mathbf{M},w\Vdash\diamondsuit p$,
h� um $w'$ com $Rww'$ tal que $\mathbf{M},w'\Vdash p$. Uma vez
que $\mathbf{M},w\Vdash\square\neg p$, temos que $\mathbf{M},w'\Vdash\neg p$,
uma contradi��o.

Para mostrar que uma f�rmula $B$ n�o implica uma outra $A$, temos
de dar um contraexemplo, ou seja, um modelo $\mathbf{M}=<W,R,V>$
em que mostramos que em algum mundo $w\in W$, $\mathbf{M},w\Vdash B$,
mas $\mathbf{M},w\nVdash A$. Considere o modelo na Figura \ref{figura2}.
Temos que $\mathbf{M},w_{1}\Vdash\diamondsuit p$ e, assim, $\mathbf{M},w_{1}\Vdash p\rightarrow\diamondsuit p$.
Entretanto, uma vez que $\mathbf{M},w_{1}\Vdash\square p$, mas $\mathbf{M},w_{1}\nVdash p$,
temos que $\mathbf{M},w_{1}\nVdash\square p\rightarrow p$.

Frequentemente exemplos bastante simples s�o suficientes. O modelo
$\mathbf{M'}=\{W',R',V'\}$ com $W'=\{w\}$, $R'=\emptyset$ e $V(p)=\emptyset$
� tamb�m um contraexemplo: uma vez que $\mathbf{M'},w\nVdash p$,
ent�o $\mathbf{M'},w\Vdash p\rightarrow\diamondsuit p$. Como nenhum
mundo � acess�vel a partir de $w$, temos que $\mathbf{M'},w\Vdash\square p$
e, assim, que $\mathbf{M'},w\nVdash\square p\rightarrow p$.
\end{example}

\begin{figure}
\begin{centering}
 \psscalebox{.7 .7} % Change this value to rescale the drawing. 
{
\begin{pspicture}(0,-3.6)(10.17,3.6) 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](1.2,2.4){1.2}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](8.4,2.4){1.2}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.8,-2.4){1.2} 
\rput[bl](0.8,2.4){$w_2$} 
\rput[bl](8.0,2.4){$w_3$} 
\rput[bl](4.4,-2.8){$w_1$}
\rput[bl](2.8,2.4){$p$} 
\rput[bl](10.0,2.4){$p$}
\rput[bl](6.4,-2.4){$\neg p$}
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(3.6,-1.2)(2.0,1.2)
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(6.0,-1.2)(8.0,1.2) 
\end{pspicture} 
}
\par\end{centering}
\caption{Contraexemplo para $p\rightarrow\diamondsuit p\protect\models\square p\rightarrow p$}

\label{figura2}

\end{figure}


\section{Problema}

\textbf{Problema 1.1} Considere o modelo da Figura \ref{fig:simples}.
Quais das seguintes afirma��es valem?
\begin{enumerate}
\item $\mathbf{M},w_{1}\Vdash q$;
\item $\mathbf{M},w_{3}\Vdash\neg q$;
\item $\mathbf{M},w_{1}\Vdash p\vee q$;
\item $\mathbf{M},w_{1}\Vdash\square(p\vee q)$;
\item $\mathbf{M},w_{3}\Vdash\square q$;
\item $\mathbf{M},w_{3}\Vdash\square\bot$;
\item $\mathbf{M},w_{1}\Vdash\lozenge q$;
\item $\mathbf{M},w_{1}\Vdash\square q$
\item $\mathbf{M},w_{1}\Vdash\neg\square\square\neg q$
\end{enumerate}
\textbf{Problema 1.2} Complete a prova da Proposi��o \ref{proposicao1.7}

\noindent \textbf{Problema 1.3} Seja $\mathbf{M}=<W,R,V>$ um modelo
e suponha que $w_{1},w_{2}\in W$ s�o tais que:
\begin{enumerate}
\item $w_{1}\in V(p)$ se e somente se $w_{2}\in V(p)$; e
\item para todo $w\in W$, $Ew_{1}w$ se e somente se $Rw_{2}w$.
\end{enumerate}
Usando indu��o sobre f�rmulas, mostre que para qualquer f�rmula $A$:
$\mathbf{M},w_{1}\Vdash A$ se e somente se $\mathbf{M},w_{2}\Vdash A$.

\noindent \textbf{Problema 1.4} Seja $\mathbf{M}=<W,R,V>$. Mostre
que $\mathbf{M},w\Vdash\neg\diamondsuit A$ se e somente se $\mathbf{M},w\Vdash\square\neg A$.

\noindent \textbf{Problema 1.5} Considere o seguinte modelo $\mathbf{M}$
para a linguagem que cont�m $p_{1},p_{2},p_{3}$ como as �nicas vari�veis
proposicionais:
\begin{center}
 \psscalebox{.7 .7} % Change this value to rescale the drawing. 
{
\begin{pspicture}(0,-4.630786)(12.22,4.630786)
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](2.24,1.6492139){1.46}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](10.1,1.709214){1.46} 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](6.1,-3.1707861){1.46} 
\rput[bl](1.92,1.5092139){$w_1$} 
\rput[bl](10.0,1.549214){$w_3$} 
\rput[bl](5.96,-3.350786){$w_2$}
\rput[bl](0.26,1.989214){$p_1$} 
\rput[bl](0.04,1.549214){$\neg p_2$}
\rput[bl](0.0,1.109214){$\neg p_3$} 
\rput[bl](11.92,2.009214){$p_1$}
\rput[bl](11.92,1.5092139){$p_2$}
\rput[bl](11.92,1.0092139){$p_3$}
\rput[bl](8.14,-2.790786){$p_1$}
\rput[bl](8.14,-3.290786){$p_2$} 
\rput[bl](7.96,-3.730786){$\neg p_3$}
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(7.2,-1.890786)(9.08,0.36921397) \psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(2.94,0.12921396)(4.7,-2.090786) \psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(3.8,1.789214)(8.4,1.789214) 
\rput{-43.384533}(0.06654787,7.865721){\psarc[linecolor=black, linewidth=0.04, dimen=outer, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{<-}(9.92,3.8492138){0.68}{0.0}{270.0}} 
\end{pspicture} 
}
\par\end{center}

\noindent As seguinte f�rmulas e esquemas s�o verdadeiras no modelo
$\mathbf{M}$, ou seja, verdadeiras em qualquer mundo em $\mathbf{M}$?
Explique.
\begin{enumerate}
\item $p\rightarrow\diamondsuit p$ (para $p$ at�mica);
\item $A\rightarrow\diamondsuit A$ (para $A$ arbitr�ria);
\item $\square p\rightarrow p$ (para $p$ at�mica);
\item $\neg p\rightarrow\lozenge\square p$ (para $p$ at�mica);
\item $\diamondsuit\square A$ (para $A$arbitr�ria);
\item $\diamondsuit\square p$ (para $p$ at�mica).
\end{enumerate}
\textbf{Problema 1.7} Mostre que $A\rightarrow\square A$ � valida
na classe $\mathscr{C}$ de modelos $\mathbf{M}=<W,R,V>$, em que
$W=\{w\}$. Similarmente mostre que $B\rightarrow\square A$ e $\diamondsuit A\rightarrow B$
s�o v�lidas na classe de modelos $\mathbf{M}=<W,R,V>$, em que $R=\emptyset$.

\noindent \textbf{Problema 1.8} Prove a Proposi��o \ref{proposicao1.19}

\noindent \textbf{Proposi��o 1.9} Prove a reivindica��o na parte ``somente
se'' da prova da Proposi��o \ref{proposicao1.21} (dica: use indu��o
sobre $A$).

\noindent \textbf{Proposi��o 1.10} Mostre que nenhuma das seguintes
f�rmulas s�o v�lidas:
\begin{enumerate}
\item[D:]  $\square p\rightarrow\diamondsuit p$;
\item[T:] $\square p\rightarrow p$;
\item[B:] $p\rightarrow\square\diamondsuit p$;
\item[4:] $\square p\rightarrow\square\square p$;
\item[5:] $\diamondsuit p\rightarrow\square\diamondsuit p$.
\end{enumerate}
\textbf{Problema 1.11} Prove que os esquemas na primeira coluna da
tabela \ref{tabela1.1} s�o v�lidos e os das segunda coluna s�o inv�lidos.

\noindent \textbf{Problema 1.12} Decida se os seguintes esquemas s�o
v�lidos ou inv�lidos:
\begin{enumerate}
\item $(\diamondsuit A\rightarrow\square B)\rightarrow(\square A\rightarrow\square B)$;
\item $\diamondsuit(A\rightarrow B)\vee\square(B\rightarrow A)$.
\end{enumerate}
\textbf{Problema 1.13} Para cada um dos seguintes esquemas, encontre
um modelo $\mathbf{M}$ tal que qualquer inst�ncia da f�rmula � verdadeira
em $\mathbf{M}$:
\begin{enumerate}
\item $p\rightarrow\diamondsuit\diamondsuit p$
\item $\diamondsuit p\rightarrow\square p$
\end{enumerate}
\textbf{Problema 1.14} Mostre que $\square(A\wedge B)\models\square A$.

\noindent \textbf{Problema 1.15} Mostre que $\square(p\rightarrow q)\nvDash p\rightarrow\square q$
e $p\rightarrow\square q\nvDash\square(p\rightarrow q)$.

\chapter{Definabilidade de estrutura {[}Frame definability{]}}
\end{document}
